$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$).
\\[0ex]msg{-}spec{-}loc{-}decl(${\it snd}$;$i$;${\it da}$) $\in$ Prop